#include "PDTIfElse.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

void
PDTIfElse::setCondition(PDTExpBool & condition)
{
  addChild(&condition);
  condition.addParent(this);
}

void
PDTIfElse::setIfResult(PDTStatement &ifResult)
{
  addChild(&ifResult);
  ifResult.addParent(this);
}

void
PDTIfElse::setElseResult(PDTStatement &elseResult)
{
  addChild(&elseResult);
  elseResult.addParent(this);
}

PDTExpBool *
PDTIfElse::getCondition() const
{
  return dynamic_cast<PDTExpBool *> (children[0]);
}

PDTStatement *
PDTIfElse::getIfResult() const
{
  return dynamic_cast<PDTStatement *> (children[1]);
}

PDTStatement *
PDTIfElse::getElseResult() const
{
  return dynamic_cast<PDTStatement *> (children[2]);
}

PDTIfElse::PDTIfElse(PDTCodeGraph & CG, PDTExpBool & condition,
    PDTStatement & ifResult, PDTStatement & elseResult) :
  PDTStatement(CG)
{
  addChild(&condition);
  condition.addParent(this);

  addChild(&ifResult);
  ifResult.addParent(this);

  addChild(&elseResult);
  elseResult.addParent(this);
  Z3guard=Z3if=Z3else=Z3endif=Z3endelse=Z3closeif=NULL;
}

Z3_ast
PDTIfElse::Z3NodeVisit (PDTZ3Visitor &ZV)
{

  if (Z3node != NULL)
    return Z3node;

  PDTNode* cond = getCondition();

  char * name = cond->makeUniqueName("guard");
  Z3guard = ZV.makeStatement(name);
  ZV.current = Z3guard;

  Z3_ast Z3cond = cond->Z3visit(ZV);
  /* make sure boolean and arithmetic operations
   will use Vs2i and current
   and s2i should relate guard to condition*/

  /*
   * if ( guard_statement cond ) { if_statement body endif_statement } else { else_statement body endelse_statement } close_if
   */
  name = makeUniqueName("if");
  Z3if = ZV.makeStatement(name);

  name = makeUniqueName("else");
  Z3else = ZV.makeStatement(name);

  name = makeUniqueName("endif");
  Z3endif = ZV.makeStatement(name);

  name = makeUniqueName("endelse");
  Z3endelse = ZV.makeStatement(name);

  name = makeUniqueName("closeif");
  Z3closeif = ZV.makeStatement(name);

  /*
   *  assert the execution order between the statements based on the conditions
   *  Z3if       > ( Z3cond ? Z3guard : infinity)
   *  Z3closeif  > ( Z3cond ? Z3endif : endelse)
   *  Z3else     > ( Z3cond ? Infinity : Z3guard)
   */
  ZV.assertConditionalOrder(Z3cond, Z3if, Z3guard, ZV.Infinity);
  ZV.assertConditionalOrder(Z3cond, Z3closeif, Z3endif, Z3endelse);
  ZV.assertConditionalOrder(Z3cond, Z3else, ZV.Infinity, Z3guard);

  /*
   * The Z3Visit of the ifResult will assert the needed
   * order between Z3if (pointed to by ZV.current) and its
   * statements as it is a list of statements.
   *
   * The Z3Visit of the ifResult node will return the last statement
   * in the then body.
   * TODO: Maybe it is better to set ZV.current to that?
   *
   *  We use the lastIf to assert the order with the endif.
   *  We do  the same for lastelse.
   */
  ZV.current = Z3if;
  Z3_ast lastIf = getIfResult()->Z3visit(ZV);
  ZV.assertOrder(lastIf, Z3endif);

  ZV.current = Z3else;
  Z3_ast lastElse = getElseResult()->Z3visit(ZV);
  ZV.assertOrder(lastElse, Z3endelse);

  ZV.current = Z3closeif;
  Z3node = Z3closeif;

  return Z3node;
}

